package za.ac.sun.cs.distrib;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.search.Search;
import gov.nasa.jpf.vm.RestorableVMState;
import gov.nasa.jpf.vm.VM;

public class TreeSearch extends Search {

	private int path_limit = 0;

	private boolean resetSearch;

	public TreeSearch(Config config, VM vm) {
		super(config, vm);
		path_limit = config.getInt("search.TreeSearch.path_limit", 0);
		if (config.getBoolean("search.TreeSearch.useFlags", false)) {
			TreeFlagListener simulateListener = new TreeFlagListener(config);
			vm.addListener(simulateListener);
			addListener(simulateListener);
		} else {
			TreeCountListener simulateListener = new TreeCountListener(config);
			vm.addListener(simulateListener);
			addListener(simulateListener);
		}
	}

	public void search() {
		int depth = 0;
		int paths = 0;
		depth++;
		resetSearch = false;
		if (hasPropertyTermination()) {
			return;
		}
		RestorableVMState init_state = vm.getRestorableState();
		notifySearchStarted();
		while (!done) {
			if ((depth < depthLimit) && forward()) {
				notifyStateAdvanced();
				if (currentError != null) {
					notifyPropertyViolated();
					if (hasPropertyTermination()) {
						return;
					}
				}
				depth++;
				if (resetSearch) {
					resetSearch = false;
					paths++;
					if (paths % 10 == 0) {
						System.out.println("paths = " + paths);
					}
					depth = 1;
					vm.restoreState(init_state);
					vm.resetNextCG();
				}
			} else { // no next state or reached depth limit
				if (depth >= depthLimit) {
					notifySearchConstraintHit("depth limit reached: "
							+ depthLimit);
				}
				if (isDone() || ((path_limit > 0) && (paths >= path_limit))) {
					done = true;
				} else {
					paths++;
					if (paths % 10 == 0) {
						System.out.println("paths = " + paths);
					}
					depth = 1;
					vm.restoreState(init_state);
					vm.resetNextCG();
				}
			}
		}
		System.out.println("paths = " + paths);
		notifySearchFinished();
	}

	public void resetSearch() {
		resetSearch = true;
	}

}
